The Homotopy Type Theory Electronic Seminar Talks, abbreviated as HoTTEST, is a series of talks on various topics related to homotopy type theory and dependent type theory more generally, run by Carlo Angiuli, Dan Christensen, Chris Kapulkin, and Emily Riehl.
Peter LeFanu Lumsdaine, Inverse diagram models of type theory, 15 February 2018 (video, slides)
Emily Riehl, The synthetic theory of infinity-categories vs the synthetic theory of infinity-categories, 1 March 2018, (video, slides)
on synthetic (infinity,1)-category theory in simplicial type theory and infinity-cosmos theory
Carlo Angiuli, Computational semantics of Cartesian cubical type theory, 15 March 2018 (video, slides)
Ulrik Buchholtz, From Higher Groups to Homotopy Surfaces, 29 March 2018 (video, slides)
Michael Shulman, Type 2-theories, 12 April 2018 (video, slides)
Martín Hötzel Escardó, Constructive mathematics in univalent type theory, 26 April 2018 (video, slides)
Thorsten Altenkirch, Towards higher models and syntax of type theory, 10 May 2018 (video, slides)
Thierry Coquand, A survey of constructive models of univalence, 24 May 2018 (video, slides)
Andy Pitts, Axiomatizing Cubical Sets Models of Univalent Foundations, 20 September 2018 (video, slides)
Dimitris Tsementzis, First-Order Logic with Isomorphism, 27 September 2018 (video)
Kuen-Bang Hou, Towards efficient cubical type theory, 11 October 2018 (video, slides)
Nicolai Kraus, Some connections between open problems, 25 October 2018 (video, slides)
Guillaume Brunerie, Computer-generated proofs for the monoidal structure of the smash product, 8 November 2018 (video, slides)
Floris van Doorn, Towards Spectral Sequences for Homology, 22 November 2018 (video, slides)
Eric Finster, Towards Higher Universal Algebra in Type Theory, 6 December 2018 (video, slides)
Nicola Gambino, From algebraic weak factorisation systems to models of type theory, 31 January 2019 (slides)
Nima Rasekh, Algebraic Topology in an Elementary Higher Topos, 7 February 2019 (video, slides)
Simon Huber, Homotopy canonicity for cubical type theory, 21 February 2019 (video, slides)
Evan Cavallo, Internal Parametricity and Cubical Type Theory, 7 March 2019 (video, slides)
Dan Licata, A Fibrational Framework for Substructural and Modal Dependent Type Theories, 21 March 2019 (video, slides)
Joachim Kock, Infinity-operads as polynomial monads, 4 April 2019 (video, lecture notes)
Paolo Capriotti, Polynomial monads as opetopic types, 18 April 2019 (video, lecture notes)
Mathieu Anel, Descent v. Univalence, 2 May 2019 (video, slides)
Andrej Bauer, General type theories, 9 October 2019 (video, slides)
Anders Mörtberg, Unifying Cubical Models of Homotopy Type Theory, 23 October 2019 (video, slides)
Andrew Swan, Choice, Collection and Covering in Cubical Sets, 6 November 2019 (video, slides)
Benno van den Berg, Uniform Kan fibrations in simplicial sets, 20 November 2019 (video, slides)
Richard Garner, Polynomial comonads and comodules, 11 December 2019 (video, slides)
Simon Henry, The language of a model category, 23 January 2020 (video, slides)
Niels van der Weide, Constructing 1-Truncated Finitary Higher Inductive Types as Groupoid Quotients, 6 February 2020 (video, slides)
Karol Szumiło, The Constructive Kan-Quillen Model Structure, 20 February 2020 (video, slides)
Jon Sterling, Objective Metatheory of Dependent Type Theories, 19 March 2020 (video, slides)
Denis-Charles Cisinski, Univalence of the universal coCartesian fibration, 2 April 2020 (video, slides)
Matthew Weaver, A constructive model of directed univalence in bicubical sets, 16 April 2020 (video, slides)
Guillaume Brunerie, Peter LeFanu Lumsdaine, Initiality for Martin-Löf type theory, 10 September 2020 (video, slides-GB, slides-PLL)
Jakob von Raumer, Coherence via Well-Foundedness, 24 September 2020 (video, slides)
Yuki Maehara, A cubical model for weak omega-categories, 8 October 2020 (video, slides)
Ambrus Kaposi, Quotient inductive-inductive types and higher friends, 22 October 2020 (video, slides)
Nima Rasekh, Filter Products and Elementary Models of Homotopy Type Theory, 5 November 2020 (video, slides)
Pierre Cagne, On the symmetries of the spheres in univalent foundations, 19 November 2020 (video, slides)
Jamie Vicary, A type theory for strictly unital infinity-categories, 3 December 2020 (video, slides)
Thierry Coquand, Sheaf models and constructive mathematics, 28 January 2021 (video, slides)
Norihiro Yamada, Game semantics of homotopy type theory, 11 February 2021 (video, slides)
Carlo Angiuli, Internalizing Representation Independence with Univalence, 25 February 2021 (video, slides)
Andrea Vezzosi, Cubical Agda and its Extensions, 11 March 2021 (video, Agda files)
Håkon Robbestad Gylterud, Defining and relating theories, 25 March 2021 (video, slides)
Egbert Rijke, A higher encode decode method, 8 April 2021 (video, slides)
Ulrik Buchholtz, (Co)cartesian families in simplicial type theory, 22 April 2021 (video, slides)
Rafaël Bocquet, Coherence of definitional equality in type theory, 23 September 2021 (video, slides)
Matthieu Sozeau, The MetaCoq Project, 7 October 2021 (video, slides)
Hugo Moeneclaey, Parametricity and cubes, 21 October 2021 (video, slides)
Kristina Sojakova, Syllepsis in Homotopy Type Theory, 4 November 2021 (video, slides)
Raffael Stenzel, Higher sites and their higher categorical logic, 18 November 2021 (video, slides)
Taichi Uemura, Infinity-type theories and internal language conjectures, 2 December 2021 (video, slides)
Jonas Frey, Characterizing clan-algebraic categories, 3 February 2022 (video, slides)
Marcelo Fiore, Mathematical and Computational Metatheory of Second-Order Algebraic Theories, 17 February 2022 (video, slides)
Fredrik Nordvall Forsberg, Different Notions of Ordinals in Homotopy Type Theory, 3 March 2022 (video, slides)
Chaitanya Leena Subramaniam, Dependently typed algebraic theories and their homotopy algebras, 17 March 2022 (video, slides)
Assia Mahboubi, Continuity in dependent type theory, 31 March 2022 (slides)
Amélia Liao, Univalent Category Theory, 6 October 2022, (slides, video)
on category theory in univalent cubical type theory in the 1lab
Chris Grossack, Where are the open sets? Comparing HoTT with Classical Topology, 6 October 2022, (slides, video)
Max Zeuner, A univalent formalization of affine schemes, 20 October 2022 (slides, video)
Axel Ljungström, Calculating a Brunerie Number, 20 October 2022 (slides, video)
Evan Cavallo, Cubes with one connection and relative elegance, 3 November 2022 (slides, video)
Colin Zwanziger, Hofmann-Streicher Universes via Coalgebra, 3 November 2022 (slides, video)
Tom de Jong, Acyclic types and epimorphisms in HoTT, 17 November 2022 (slides, video)
Jarl G. Taxerås Flaten, Central H-spaces and banded types, 17 November 2022 (slides, video).
Jacob Neumann, (Co)ends and (Co)structure, 1 December 2022 (slides, video)
Astra Kolomatskaia, Semi-Simplicial Types, 15 December 2022 (slides, video)
Philipp Joram, Final Coalgebras of Analytic Functors in Homotopy Type Theory, 15 December 2022 (slides, video)
Johan Commelin, Liquid Tensor Experiment, 26 January 2023 (slides, video)
Andrew Swan, Double negation stable h-propositions in cubical sets, 9 February 2023 (slides, video)
Last revised on June 13, 2023 at 17:38:18. See the history of this page for a list of all contributions to it.